Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		bsort(nil)	→ nil
2:		bsort(x . y)	→ last(bubble(x . y) . bsort(butlast(bubble(x . y))))
3:		bubble(nil)	→ nil
4:		bubble(x . nil)	→ x . nil
5:		bubble(x . (y . z))	→ if(x ≤ y,y . bubble(x . z),x . bubble(y . z))
6:		last(nil)	→ 0
7:		last(x . nil)	→ x
8:		last(x . (y . z))	→ last(y . z)
9:		butlast(nil)	→ nil
10:		butlast(x . nil)	→ nil
11:		butlast(x . (y . z))	→ x . butlast(y . z)

There are 8 dependency pairs:


12:		BSORT(x . y)	→ LAST(bubble(x . y) . bsort(butlast(bubble(x . y))))
13:		BSORT(x . y)	→ BSORT(butlast(bubble(x . y)))
14:		BSORT(x . y)	→ BUTLAST(bubble(x . y))
15:		BSORT(x . y)	→ BUBBLE(x . y)
16:		BUBBLE(x . (y . z))	→ BUBBLE(x . z)
17:		BUBBLE(x . (y . z))	→ BUBBLE(y . z)
18:		LAST(x . (y . z))	→ LAST(y . z)
19:		BUTLAST(x . (y . z))	→ BUTLAST(y . z)

The approximated dependency graph contains 4 SCCs: {16,17}, {19}, {18} and {13}.

Consider the SCC {16,17}. There are no usable rules. By taking the AF π with π(BUBBLE) = 1 and π(.) = [2] together with the lexicographic path order with empty precedence, the rules in {16,17} are strictly decreasing.

Consider the SCC {19}. There are no usable rules. By taking the AF π with π(BUTLAST) = 1 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Consider the SCC {18}. There are no usable rules. By taking the AF π with π(LAST) = 1 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.

Consider the SCC {13}. The usable rules are {3-5,9-11}. The constraints could not be solved.

Tyrolean Termination Tool (0.27 seconds) --- May 3, 2006